package flowlogic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;

import ast.ExpVar;
import ast.Expression;
import ast.Some;
import ast.Term;

public class ExpressionJudgement extends FLJudgement {
	
	private Expression exp;
	
	private ResNode res;
	private PsiNode psi;
	
	public ExpressionJudgement(Expression e, HashMap<String, HashSet<Term>> rho)
	{
		exp = e;
		setRho(rho);
		res = new ResNode();
		psi = new PsiNode();
	}
	
	public PsiNode getPsi()
	{
		return psi;
	}
	
	public ResNode getRes()
	{
		return res;
	}
	
	public String toString()
	{
		String res = "";
		res += getRho() + " |- " + exp + " : " + psi + " & " + this.res;
		return res;
	}
	
	public ArrayList<DischargeResult> discharge()
	{
		ArrayList<DischargeResult> resList = new ArrayList<DischargeResult>();
		
		if (exp instanceof ExpVar) {
			
			FreeVariable fv = new FreeVariable(((ExpVar) exp).getName());
			resList.add(new Inclusion(new RhoNode(fv), res, true));
			
		} else if (exp instanceof Some) {
			
			TermJudgement tjg = new TermJudgement(((Some) exp).getTerm(), getRho());
			resList.add(tjg);
			PsiNode psiT = tjg.getPsi();
			ResNode resT = tjg.getRes();
			resList.add(new Inclusion(resT, res, true));
			resList.add(new Inclusion(psiT, psi, true));
			
		} else { // exp instanceof none
		}
		
		return resList;
	}

}
